We give a method to prove confluence of term rewriting systems that containnon-terminating rewrite rules such as commutativity and associativity. Usually,confluence of term rewriting systems containing such rules is proved bytreating them as equational term rewriting systems and considering E-criticalpairs and/or termination modulo E. In contrast, our method is based solely onusual critical pairs and it also (partially) works even if the system is notterminating modulo E. We first present confluence criteria for term rewritingsystems whose rewrite rules can be partitioned into a terminating part and apossibly non-terminating part. We then give a reduction-preserving completionprocedure so that the applicability of the criteria is enhanced. In contrast tothe well-known Knuth-Bendix completion procedure which preserves theequivalence relation of the system, our completion procedure preserves thereduction relation of the system, by which confluence of the original system isinferred from that of the completed system.
展开▼
